perm filename AXIOM.LSP[1,JRA]1 blob
sn#005853 filedate 1972-10-19 generic text, type T, neo UTF8
00100
00200
00300 (DEFPROP FOO
00400 (NIL FOO
00500 APPENDIT
00600 ATTEMPT
00700 ATTEMPTUNTIL
00800 ATTEMPT1
00900 AUTO
01000 CHOICE1
01100 GOLIST
01200 INCLAUSES
01300 INITIAL
01400 INITIALAX
01500 INITIALAX1
01600 NEGATE
01700 PRECNF
01800 PROOF1
01900 PROOF
02000 QUERY
02100 RESET1
02200 SAVE1
02300 SET1
02400 SETQUERY1
02500 SETQUERY2
02600 SETUP
02700 TREE
02800 TREEDEP
02900 TRY1
03000 TRAVERSE
03100 UPDATE
03200 UPGETL)
03300 VALUE)
03400
03500 (DEFPROP APPENDIT
03600 (LAMBDA(X Y)
03700 (PROG NIL (COND (USINGFL (SETQ USING (CONS N2 (APPEND (REVERSE Y) USING))))) (RETURN (APPEND X Y))))
03800 EXPR)
03900
04000 (DEFPROP ATTEMPT
04100 (LAMBDA(Z S C)
04200 (PROG (NEWNAME SUPPORT
04300 EDITSTRAT
04400 LCL
04500 LVL
04600 CNT
04700 XYZ2
04800 LSTCLS
04900 LLST
05000 Z1
05100 MERGE
05200 ORDER
05300 DEBUG
05400 DEPTH
05500 LENGTH
05600 ANCESTRY
05700 STRATEGY
05800 STRAT
05900 PMODEL
06000 NMODEL
06100 PFLG
06200 EQUAL
06300 PDEPTH
06400 DLIST
06500 XYZ
06600 XYZ1
06700 COND
06800 UNAXP
06900 UNAXN
07000 SAT
07100 EE
07200 EE1
07300 XX
07400 CLAUSES
07500 SUBCLAUSES
07600 COUNT)
07700 (SETQ TBL (SET1 (APPEND PREFN INFN)))
07800 (SET3 Z)
07900 (SETQ Z (MINIMIZE Z))
08000 (SETQ NEWNAME (INITIAL Z))
08100 (UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
08200 (SETQ COND C)
08300 (SETQ XYZ2 Z)
08400 (SETQ LVL 1)
08500 (SETQ COUNT 0)
08600 (SETQ Z (UNITPN XYZ2))
08700 (SETQ UNAXP (CAR Z))
08800 (SETQ UNAXN (CDR Z))
08900 (SETQ CLAUSES XYZ2)
09000 (COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
09100 (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
09200 (T (SETQ SUBCLAUSES CLAUSES)))
09300 (SETQ LCL (LAST CLAUSES))
09400 (SETQ LSTCLS LCL)
09500 (COND (ANCESTRY (GO AA)))
09600 (SETQ XX (CONS CLAUSES CLAUSES))
09700 (SETQ EE CLAUSES)
09800 (SETQ EE1 (LAST EE))
09900 (SETQ CNT (LENGTH XYZ2))
10000 BB (SETQ Z1 (ERRSET (ATTEMPT1 XYZ2)))
10100 (COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
10200 ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
10300 (EVAL
10400 (LIST (QUOTE OUTC)
10500 (LIST (QUOTE OUTPUT)
10600 (QUOTE PRF)
10700 (QUOTE DSK:)
10800 (CONS (READLIST
10900 (CONS (QUOTE #)
11000 (CONS (SETQ PRNO (ADD1 PRNO))
11100 FILENAM)))
11200 (QUOTE PRF)))
11300 NIL)))
11400 (QUERY)
11500 (PROOF LHP RHP)
11600 (OUTC Z T)
11700 (RETURN Z1))
11800 (T (RETURN Z1)))
11900 AA (SETQ XYZ XYZ2)
12000 (SETQ EE CLAUSES)
12100 (SETQ EE1 (LAST CLAUSES))
12200 CC (SETQ LLST (CONS (CAR XYZ) LLST))
12300 (SETQ XYZ (CDR XYZ))
12400 (COND (XYZ (GO CC)) (T (GO BB)))))
12500 EXPR)
12600
12700 (DEFPROP ATTEMPTUNTIL
12800 (LAMBDA (L S C) (ATTEMPT (INITIALAX L) S C))
12900 EXPR)
13000
13100 (DEFPROP ATTEMPT1
13200 (LAMBDA (L) (COND (ANCESTRY (ANCESTRY LLST)) (T (TRYPRF L))))
13300 EXPR)
13400
13500 (DEFPROP AUTO
13600 (LAMBDA(XX)
13700 (PROG (X1 Z2 D M STRATEGY SUPPORT EDITSTRAT MERGE ORDER DEBUG ANCESTRY PMODEL NMODEL PFLG PDEPTH DLIST)
13800 (COND (EQUAL (SETQ PFLG NIL)) (T (SETQ PFLG NIL)))
13900 (SETQ PDEPTH 3)
14000 (SETQ DDEPTH 4)
14100 (COND
14200 ((NULL EQUAL) (PRINT (QUOTE (IS THERE AN EQUALITY PREDICATE (Y / N))))
14300 (COND
14400 ((EQ (READ) (QUOTE Y)) (PRINT (QUOTE (WHAT IS IT)))
14500 (SETQ PFLG NIL)
14600 (SETQ EQUAL (READ))))))
14700 (SETQ X1 XX)
14800 (SETQ M (SETQ D 0))
14900 A (SETQ M (MAX M (LENGTH (CDAR X1))))
15000 (SETQ D (MAX D (DEPTH (CDAR X1))))
15100 (SETQ Z2 (CAR X1))
15200 (COND
15300 ((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
15400 (SETQ DLIST (CONS (CONS (CONS (CAAAR Z2) (CDAR Z2)) (CDR Z2)) DLIST))))
15500 (SETQ X1 (CDR X1))
15600 (COND ((CDR X1) (GO A)))
15700 (SETQ Z2 (ASSOC (QUOTE THEOREM) NEWNAME))
15800 (COND ((NULL Z2) (GO C)) (T (SETQ Z2 (CDR Z2))))
15900 B (COND (Z2 (SETQ SUPPORT (CONS (CDAR Z2) SUPPORT)) (SETQ Z2 (CDR Z2)) (GO B)))
16000 C (COND ((NULL LENGTH) (SETQ LENGTH (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2)))
16100 ((ZEROP ITER) (SETQ LENGTH (ADD1 LENGTH))))
16200 (COND ((NOT (GREATERP LENGTH 0)) (SETQ LENGTH 1)))
16300 (COND ((NULL DEPTH) (SETQ DEPTH (ADD1 D))) ((NOT (ZEROP ITER)) (SETQ DEPTH (ADD1 DEPTH))))
16400 (COND ((ZEROP ITER) (SETQ ITER 1)) (T (SETQ ITER 0)))
16500 (COND (SUPPORT (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))))
16600 (SETQ ANCESTRY T)
16700 (SETQ EDITSTRAT
16800 (QUOTE (LAMBDA (C) (OR (GREATERP (LENGTH (CDR C)) LENGTH) (GREATERP (DEPTH (CDR C)) DEPTH)))))
16900 (SETQ DEBUG T)
17000 (COND (DLIST (SET3 DLIST)))
17100 (RETURN
17200 (LIST STRATEGY
17300 SUPPORT
17400 EDITSTRAT
17500 MERGE
17600 ORDER
17700 DEBUG
17800 DEPTH
17900 LENGTH
18000 ANCESTRY
18100 PMODEL
18200 NMODEL
18300 PFLG
18400 EQUAL
18500 PDEPTH
18600 DLIST))))
18700 EXPR)
18800
18900 (DEFPROP AUTO
19000 (NIL . T)
19100 VALUE)
19200
19300 (DEFPROP CHOICE1
19400 (LAMBDA (L LL) (COND ((ATOM (CDR (ANCESTOR L))) LL) (T (NCONC (CDR (TRAVERSE L)) LL))))
19500 EXPR)
19600
19700 (DEFPROP GOLIST
19800 (NIL (EO . UEO1)
19900 (DS . UDS1)
20000 (CH . UCH1)
20100 (SY . USY1)
20200 (CU . UCU1)
20300 (FL . UFL1)
20400 (DI . UDI1)
20500 (ST . UST1)
20600 (HA . UST1)
20700 (DE . UDE1)
20800 (IN . UIN1)
20900 (EV . UEV1)
21000 (QU . UQU1)
21100 (TR . UTR1)
21200 (UP . UUP1)
21300 (ME . UME1)
21400 (SI . USI1)
21500 (SE . USE1)
21600 (DO . UDO1)
21700 (CL . UCL1)
21800 (SU . USU1)
21900 (AN . UAN1)
22000 (TE . UTE1)
22100 (RE . URE1)
22200 (SA . USA1)
22300 (PA . UPA1)
22400 (AS . UAS1)
22500 (ED . UED1)
22600 (US . UUS1)
22700 (PR . UPR1)
22800 (FU . UFL2)
22900 (FD . UFL3)
23000 (GO . UGO1)
23100 (EX . UEX1)
23200 (AB . UAB1)
23300 (HE . UHE1))
23400 VALUE)
23500
23600 (DEFPROP INCLAUSES
23700 (LAMBDA NIL
23800 (PROG (Z AXNO)
23900 (SETQ AXNO (QUOTE AXIOM))
24000 A (SCANSET)
24100 (START)
24200 (SETQ ZIN (ERRSET (<INPUT>) T))
24300 (SCANRESET)
24400 (COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
24500 (SETQ ZIN (TOP))
24600 (COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z)) ((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A)))
24700 (OUT >S< ZIN)
24800 (SETQ Z
24900 (APPEND Z
25000 (SETUP
25100 (CNF
25200 (COND ((EQ AXNO (QUOTE THEOREM)) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
25300 (GO A)))
25400 EXPR)
25500
25600 (DEFPROP INITIAL
25700 (LAMBDA(L)
25800 (PROG (ST Z Z1 Z2)
25900 A (SETQ Z (CDR (ANCESTOR (CAR L))))
26000 (COND ((NOT (ATOM Z)) (PRINT (QUOTE LOSE-IN-INITIAL)) (ERR NIL))
26100 ((SETQ Z1 (ASSOC Z ST)) (RPLACD (LAST Z1) (LIST (CAR L))))
26200 (T (SETQ ST (CONS (CONS Z (LIST (CAR L))) ST))))
26300 (SETQ Z2 (CONS (CAR L) Z2))
26400 (SETQ L (CDR L))
26500 (COND (L (GO A)))
26600 (RETURN (REVERSE (CONS (CONS NIL NIL) (CONS (CONS (QUOTE %INITIAL) (REVERSE Z2)) ST))))))
26700 EXPR)
26800
26900 (DEFPROP INITIALAX
27000 (LAMBDA(L)
27100 (PROG (Z Z1 Z2 Z3 AXNO)
27200 (SETQ AXNO (CAR L))
27300 (SETQ L (CDR L))
27400 A (SETQ Z (CAR (SETUP (LIST (COPY (CDAR L))))))
27500 (SETQ Z1 (ANCESTOR (CAR L)))
27600 (COND ((ATOM (CAR Z1)) (SETQ Z1 (CDR Z1))))
27700 (SETQ Z2 (ANCESTOR Z))
27800 (RPLACA Z2 Z1)
27900 (RPLACD Z2 AXNO)
28000 (SETQ Z3 (CONS Z Z3))
28100 B (SETQ L (CDR L))
28200 (COND ((NULL L) (RETURN (REVERSE Z3))) ((ATOM (CAR L)) (SETQ AXNO (CAR L)) (GO B)))
28300 (GO A)))
28400 EXPR)
28500
28600 (DEFPROP INITIALAX1
28700 (LAMBDA(L1)
28800 (PROG (Z L2 L)
28900 (SETQ L L1)
29000 B1 (SETQ L2 L)
29100 A1 (COND ((EQ (CAR L) (CADR L2)) (RPLACD L2 (CDDR L2)) (GO A1)))
29200 (SETQ L2 (CDR L2))
29300 (COND (L2 (GO A1)))
29400 (SETQ L (CDR L))
29500 (COND (L (GO B1)))
29600 (SETQ L L1)
29700 B (SETQ Z (CDDAAR L))
29800 (COND ((NULL (CAAAR L)) (RPLACA (CAAR L) (LENGTH (CDAR L))))
29900 ((NUMBERP (CAAAR L)) NIL)
30000 (T (RPLACA (CAAR L) (CAAAAR L))))
30100 (COND ((ATOM (CDDR Z)) (GO A)))
30200 (RPLACD Z (CONS (CDR Z) (QUOTE DEDUCT)))
30300 A (SETQ L (CDR L))
30400 (COND (L (GO B)))
30500 (RETURN L1)))
30600 EXPR)
30700
30800 (DEFPROP NEGATE
30900 (LAMBDA(Z)
31000 (PROG (BDY)
31100 A (SETQ Z (CDR Z))
31200 (COND ((EQ (LENGTH Z) 1) (SETQ BDY (FIXNEG (CAR Z))) (GO D)))
31300 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CADR Z)) (FIXNEG (CAR Z))))
31400 (SETQ Z (CDDR Z))
31500 C (COND ((NULL Z) (GO D)))
31600 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CAR Z)) BDY))
31700 (SETQ Z (CDR Z))
31800 (GO C)
31900 D (RETURN (SET3 (SETUP (CNF (LIST (QUOTE NOT) (FIXQFF BDY))))))))
32000 EXPR)
32100
32200 (DEFPROP PRECNF
32300 (LAMBDA(X)
32400 (COND ((EQ (CAR X) (QUOTE NOT)) (LIST (QUOTE NOT) (PRECNF (CADR X))))
32500 ((MEMQ (CAR X) (QUOTE (AND OR))) (LIST (CAR X) (PRECNF (CADR X)) (PRECNF (CADDR X))))
32600 ((MEMQ (CAR X) (QUOTE (FA TE))) (LIST (CAR X) (CADR X) (PRECNF (CADDR X))))
32700 ((EQ (CAR X) (QUOTE IMP)) (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X))))
32800 ((EQ (CAR X) (QUOTE EQUIV))
32900 (LIST (QUOTE AND)
33000 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X)))
33100 (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (COPY (CADDR X)))) (PRECNF (COPY (CADR X))))))
33200 (T X)))
33300 EXPR)
33400
33500 (DEFPROP PROOF1
33600 (LAMBDA(L)
33700 (PROG (Q X Y Z P P1)
33800 (PRINC (QUOTE / ))
33900 (PRINC (QUOTE / ))
34000 (PRFPRINT (CDR L))
34100 (SETQ P (ANCESTOR L))
34200 (COND ((ATOM (CDR P)) (GO P3)))
34300 (SETQ P1 (CDR P))
34400 (SETQ P (CAR P))
34500 (PRINC (QUOTE / ))
34600 (PRINC 1)
34700 (PRINC (QUOTE / ))
34800 (PRINC 2)
34900 (SETQ X 1)
35000 (SETQ Y 2)
35100 (SETQ Q (LIST (CONS X P) (CONS Y P1)))
35200 P1 (SETQ Z (ANCESTOR (CDAR Q)))
35300 (COND ((ATOM (CDR Z)) (PRINT (CAAR Q)) (PRFPRINT (CDDAR Q)) (PRIN1 (CDR Z)) (GO P2)))
35400 (SETQ X (ADD1 Y))
35500 (SETQ Y (ADD1 X))
35600 (PRINT (CAAR Q))
35700 (PRFPRINT (CDDAR Q))
35800 (PRINC X)
35900 (PRINC (QUOTE / ))
36000 (PRINC Y)
36100 (SETQ Q (NCONC Q (LIST (CONS X (CAR Z)) (CONS Y (CDR Z)))))
36200 P2 (SETQ Q (CDR Q))
36300 (COND ((NULL Q) (RETURN NIL)))
36400 (GO P1)
36500 P3 (PRIN1 (CDR P))
36600 (RETURN (TERPRI))))
36700 EXPR)
36800
36900 (DEFPROP PROOF
37000 (LAMBDA(L R)
37100 (PROG (Q Q1 X Z)
37200 (SETQ LHP L)
37300 (SETQ RHP R)
37400 (RPLACA (MKWRD L) 1)
37500 (RPLACA (MKWRD R) 2)
37600 (SETQ X 2)
37700 (SETQ Q (LIST L R))
37800 (SETQ Q1 Q)
37900 P1 (SETQ Z (ANCESTOR (CAR Q)))
38000 (COND ((ATOM (CDR Z)) (COND ((NOT (ATOM (CAR Z))) (SETQ Z (CAR Z))) (T (GO P2)))))
38100 (RPLACA (MKWRD (CAR Z)) (SETQ X (ADD1 X)))
38200 (RPLACA (MKWRD (CDR Z)) (SETQ X (ADD1 X)))
38300 (NCONC Q (LIST (CAR Z) (CDR Z)))
38400 P2 (SETQ Q (CDR Q))
38500 (COND (Q (GO P1)))
38600 (PRINT (QUOTE NIL))
38700 (PRINC (CAR (MKWRD (CAR Q1))))
38800 (PRINC (QUOTE / ))
38900 (PRINC (CAR (MKWRD (CADR Q1))))
39000 (SETQ X 1)
39100 A (COND
39200 ((EQ (CAR (MKWRD (CAR Q1))) X) (PRINT X)
39300 (PRFPRINT (CDAR Q1))
39400 (COND
39500 ((ATOM (CAR (ANCESTOR (CAR Q1)))) (PRIN1 (CAR (ANCESTOR (CAR Q1)))))
39600 ((ATOM (CDR (ANCESTOR (CAR Q1))))
39700 (PRINC (CAR (MKWRD (CAAR (ANCESTOR (CAR Q1))))))
39800 (PRINC (QUOTE / ))
39900 (PRINC (CAR (MKWRD (CDAR (ANCESTOR (CAR Q1)))))))
40000 (T (PRINC (CAR (MKWRD (CAR (ANCESTOR (CAR Q1))))))
40100 (PRINC (QUOTE / ))
40200 (PRINC (CAR (MKWRD (CDR (ANCESTOR (CAR Q1))))))))))
40300 (SETQ Q1 (CDR Q1))
40400 (SETQ X (ADD1 X))
40500 (COND (Q1 (GO A)))))
40600 EXPR)
40700
40800 (DEFPROP QUERY
40900 (LAMBDA NIL
41000 (PROG NIL
41100 (COND (STRATEGY (PRINT (QUOTE CHOICE-STRATEGY-IS:)) (OUT >ST< (CAR (LAST STRATEGY)))))
41200 (PRINT (QUOTE EDIT-STRATEGY-IS:))
41300 (OUT >ST< (CAR (LAST EDITSTRAT)))
41400 (COND ((AND (NULL PMODEL) (NULL NMODEL)) (GRINDEF MODEL))
41500 (T (PRINT (QUOTE POSITIVE-MODEL=))
41600 (PRINC PMODEL)
41700 (PRINT (QUOTE NEGATIVE-MODEL=))
41800 (PRINC NMODEL)))
41900 (PRINT (QUOTE PARMODULATE))
42000 (PRINC (QUOTE =))
42100 (COND ((NOT PFLG) (PRINC T)
42200 (PRINT (QUOTE EQUAL-SYMBOL))
42300 (PRINC (QUOTE =))
42400 (PRINC EQUAL)
42500 (PRINT (QUOTE PAR-DEPTH-BOUND))
42600 (PRINC (QUOTE =))
42700 (PRINC PDEPTH))
42800 (T (PRINC NIL)))
42900 (PRINT (QUOTE ELAPSED-TIME))
43000 (PRINC (QUOTE =))
43100 (PRINC (TIMEIT))
43200 (RETURN (TERPRI))))
43300 EXPR)
43400
43500 (DEFPROP RESET1
43600 (LAMBDA(L)
43700 (PROG (X Z2 Z3 ZZ XX Z Z1 F1)
43800 (SETQ Z STATEVECTOR)
43900 A (COND
44000 ((EQ (CAR L) (CAR Z)) (SETQ F1 T)
44100 (COND ((EQ (CAR L) (QUOTE STRATEGY)) (GO R1))
44200 (T (SET (CAR Z) (EVAL (CADR L)))))))
44300 R2 (SETQ Z1 (CONS (EVAL (CAR Z)) Z1))
44400 (SETQ Z (CDR Z))
44500 (COND (Z (GO A)))
44600 (COND (F1 (RETURN (REVERSE Z1))))
44700 R3 (PRINT (QUOTE UNDEFINED-ARG-FOR-RESET:))
44800 (PRINC (CAR L))
44900 (TERPRI)
45000 (ERR NIL)
45100 R1 (SETQ X (QUOTE (X)))
45200 (SETQ L (CDR L))
45300 R4 (SETQ Z2 (CAR L))
45400 (COND ((ATOM Z2) (SETQ Z3 Z2)) (T (SETQ Z3 (CAR Z2))))
45500 SPQ2 (COND ((NOT (MEMQ Z3 STRATLIST)) (GO R3))
45600 ((EQ Z3 (QUOTE SUPPORT)) (SETQ XX (EVAL (CADAR L)))
45700 (PROG (ZZ)
45800 (GO B)
45900 A (SETQ ZZ (CONS (CDAR XX) ZZ))
46000 (SETQ XX (CDR XX))
46100 B (COND (XX (GO A)))
46200 (SETQ SUPPORT ZZ))
46300 (SETQ ZZ (QUOTE (SUPPORT C2))))
46400 ((EQ Z3 (QUOTE MODEL)) (SETQ PMODEL (CADAR L))
46500 (SETQ NMODEL (CADDAR L))
46600 (SETQ ZZ (CONS (CONS Z3 X) ZZ)))
46700 ((EQ Z3 (QUOTE ANCESTRY)) (SETQ ANCESTRY T))
46800 ((EQ Z3 (QUOTE ORDER)) (SETQ ORDER T))
46900 ((EQ Z3 (QUOTE MERGE)) (SETQ MERGE T))
47000 (T (SETQ ZZ (CONS (CONS Z3 X) ZZ))))
47100 (SETQ L (CDR L))
47200 (COND (L (GO R4)))
47300 (COND (ZZ (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))) (T (SETQ STRATEGY NIL)))
47400 (GO R2)))
47500 FEXPR)
47600
47700 (DEFPROP SAVE1
47800 (LAMBDA(L)
47900 (PROG (L1 N ASLST CLST Z Z2 Z3 Z4 Z5)
48000 (SETQ N 0)
48100 (SETQ Z L)
48200 A (SETQ ASLST (CONS (CONS (CAR L) N) ASLST))
48300 (SETQ L (CDR L))
48400 (SETQ N (ADD1 N))
48500 (COND (L (GO A)))
48600 (SETQ CLST (LAST Z))
48700 (SETQ L Z)
48800 B (SETQ Z2 (CAAR L))
48900 (COND ((NULL (CAR Z2)) (SETQ Z3 NIL)) (T (SETQ Z3 (CAAR Z2))))
49000 (COND ((NULL (CADR Z2)) (SETQ Z4 NIL))
49100 (T
49200 (SETQ Z4
49300 (PROG (Z Z1 N)
49400 (SETQ N 0)
49500 (SETQ Z1 (CDAR L))
49600 (SETQ Z (CADR Z2))
49700 A (COND ((EQ Z Z1) (RETURN N)))
49800 (SETQ Z1 (CDR Z1))
49900 (SETQ N (ADD1 N))
50000 (GO A)))))
50100 (SETQ Z (CDDDR Z2))
50200 (COND ((ATOM (CDR Z))
50300 (COND ((NOT (ATOM (CAR Z))) (SETQ Z5 (UNWIND (CAAR Z) (CDAR Z) CLST ASLST N))
50400 (SETQ N (CDR Z5))
50500 (SETQ Z5 (CONS NIL (CAR Z5))))
50600 (T (SETQ Z5 (LIST Z)))))
50700 (T (SETQ Z2 (UNWIND (CAR Z) (CDR Z) CLST ASLST N)) (SETQ Z5 (CAR Z2)) (SETQ N (CDR Z2))))
50800 (SETQ Z (CONS Z3 (CONS Z4 (CONS 0 Z5))))
50900 (SETQ L1 (CONS (CONS Z (CDAR L)) L1))
51000 C (SETQ L (CDR L))
51100 (COND (L (GO B)))
51200 (RPLACD CLST NIL)
51300 (RETURN (REVERSE L1))))
51400 EXPR)
51500
51600 (DEFPROP SET1
51700 (LAMBDA(L)
51800 (PROG (TBL N)
51900 (SETQ N 1)
52000 (SETQ ZERO (CDAR (SETU (LIST (CONS 0 0)))))
52100 A (SETQ TBL (CONS (CONS (CAR L) N) TBL))
52200 (SETQ L (CDR L))
52300 (COND (L (SETQ N (ADD1 N)) (GO A)))
52400 (RETURN (SETU TBL))))
52500 EXPR)
52600
52700 (DEFPROP SETQUERY1
52800 (LAMBDA(X Y)
52900 (PROG (Z)
53000 (SETQ Z (ERRSET (SETQUERY2 X Y T)))
53100 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (RETURN Z)))
53200 (RETURN (CONS (QUOTE NOPROOF) (CAR Z)))))
53300 EXPR)
53310 (DE UP1B(X N)(PROG NIL(TERPRI)(PRINC N)(PRINC @/ )(PRFPRINT(CDR X))))
53320
53400
53500 (DEFPROP SETQUERY2
53600 (LAMBDA(XX YY FLG)
53700 (PROG (XYZ1 N
53800 CHAN
53900 Z
54000 Z1
54100 Z3
54200 XYZ
54300 Z6
54400 SUPPORT
54500 EDITSTRAT
54600 MERGE
54700 ORDER
54800 DEBUG
54900 DEPTH
55000 LENGTH
55100 ANCESTRY
55200 STRATEGY
55300 PMODEL
55400 NMODEL
55500 PFLG
55600 EQUAL
55700 PDEPTH
55800 DLIST)
55900 (SETQ CHAN (OUTC NIL NIL))
56000 (COND (FLG (UPDATESTATE YY)))
56100 (SETQ XYZ1 XX)
56200 (COND ((NULL FLG) (GO SRA1)) ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
56300 (PRINT SETQMESS)
56400 (SETQ XX (UPDATE XX))
56500 (SETQ XYZ1 XX)
56600 SRA1 (COND ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
56700 (PRINT (QUOTE HERE-ARE-THE-CLAUSES:))
56800 (SETQ N 1)
56900 AA (UP1B (CAR XX) N)
57000 (SETQ N (ADD1 N))
57100 (SETQ XX (CDR XX))
57200 (COND (XX (GO AA)))
57300 SRA (COND ((AND AUTO (NULL FLG)) (SETQ Z (AUTO XYZ1)) (OUTC CHAN NIL) (RETURN Z))
57400 (AUTO (PRINT (QUOTE (STILL-AUTO (Y / N))))
57500 (COND
57600 ((EQ (READ) (QUOTE Y)) (SETQ Z (CONS XYZ1 (AUTO XYZ1))) (OUTC CHAN NIL) (RETURN Z)))))
57700 SRA2 (PRINT (QUOTE DOIT-CHOICE-STRATEGY))
57800 (SCANSET)
57900 (START)
58000 (SETQ Z (ERRSET (<ST>) T))
58100 (SCANRESET)
58200 (COND ((OR (NULL Z) (NULL (CAR Z))) (PRINT (QUOTE SCREWED-STRATEGY)) (GO SRA2)))
58300 (SETQ ZIN (TOP))
58400 (SETQ STRATEGY (LIST (QUOTE LAMBDA) (QUOTE (C1 C2)) ZIN))
58500 (OUT >ST< ZIN)
58600 SRB (PRINT (QUOTE DEBUG))
58700 (PRINC (QUOTE =))
58800 (COND (FLG (RESTRAT DEBUG SRA SRAA) (PRINC DEBUG) (BARF NIL) (RESTRAT2 DEBUG SRA))
58900 (T (RESTRATS DEBUG SRA)))
59000 SRAA SRC
59100 SRD (PRINT (QUOTE DOIT-EDIT-STRATEGY))
59200 (SCANSET)
59300 (START)
59400 (SETQ Z1 (ERRSET (<ST>) T))
59500 (SCANRESET)
59600 (COND ((OR (NULL Z1) (NULL (CAR Z1))) (PRINT (QUOTE SCREWED-EDIT-STRATEGY)) (GO SRAA)))
59700 (SETQ ZIN (TOP))
59800 (SETQ EDITSTRAT (LIST (QUOTE LAMBDA) (QUOTE (C)) ZIN))
59900 (OUT >ST< ZIN)
60000 SRCA SRI
60100 (PRINT (QUOTE (UNIT-REDUCTION (Y / N))))
60200 (COND (FLG (RESTRAT UFLG SRD SRIA) (PRINC UFLG) (BARF NIL) (RESTRAT2 UFLG SRC))
60300 (T (RESTRATS UFLG SRD)))
60400 SRIA SRE
60500 (PRINT (QUOTE PARAMODULATE))
60600 (COND (FLG (PRINC (QUOTE IS))
60700 (PRINC (QUOTE / ))
60800 (COND (PFLG (PRINC (QUOTE N))) (T (PRINC (QUOTE Y))))
60900 (PRINT (QUOTE (DO YOU WANT TO PARAMODULATE (Y / N))))
61000 (SETQ Z3 (READ))
61100 (COND ((EQ Z3 (QUOTE Y)) (SETQ PFLG NIL) (GO SRDA))
61200 ((EQ Z3 (QUOTE N)) (GO SPQ5))
61300 ((EQ Z3 ESCAPE) (PRINT (QUOTE RESETTING-TO:)) (GO SRI))
61400 (T (GO SRE))))
61500 (T (PRINC (QUOTE (Y / N)))
61600 (RESTRATS Z3 SRI)
61700 (SETQ EQUAL ESCAPE)
61800 (COND ((EQ Z3 (QUOTE N)) (GO SPQ5)))))
61900 SRDA (SETQ AXNO 1)
62000 SRF (PRINT (QUOTE EQUAL-SYMBOL))
62100 (PRINC (QUOTE =))
62200 (COND (FLG (RESTRAT EQUAL SRE SREA) (PRINC EQUAL) (BARF NIL) (RESTRAT2 EQUAL SRE))
62300 (T (RESTRATS EQUAL SRE)))
62400 SREA (SETQ PFLG NIL)
62500 SRG (PRINT (QUOTE PAR-DEPTH-BOUND))
62600 (PRINC (QUOTE =))
62700 (COND (FLG (RESTRAT PDEPTH SRF SRFA) (PRINC PDEPTH) (BARF NIL) (RESTRAT2 PDEPTH SRF))
62800 (T (RESTRATS PDEPTH SRF)))
62900 SRFA P1
63000 (PRINT (QUOTE DEMODULATION-LIST))
63100 (PRINC (QUOTE =))
63200 (PRINT (QUOTE (TYPE: 'NONE' OR 'IN' (TO INSERT))))
63300 (COND (FLG (RESTRAT XYZ SRH SRHA) (PRINC XYZ) (BARF NIL) (RESTRAT2 XYZ SRH)) (T (RESTRATS XYZ SRG)))
63400 SRHA (SETQ DLIST NIL)
63500 (COND ((EQ XYZ (QUOTE NONE)) (GO SPQ6))
63600 ((EQ XYZ (QUOTE IN)) (GO P2))
63700 (T (PRINT (QUOTE UNDEFINED-SPECIFICATION-FOR-DEMOD-LIST))))
63800 (GO P1)
63900 P2 (SETQ Z3 (INCLAUSES))
64000 P2A (COND ((NULL Z3) (PRINT (QUOTE ERROR-TRY-AGAIN)) (GO P1)))
64100 P3 (SET3 (SETQ DLIST Z3))
64200 SRH (PRINT (QUOTE DEMOD-DEPTH-BOUND=))
64300 (COND (FLG (RESTRAT DDEPTH P1 SRGA) (PRINC DDEPTH) (BARF NIL) (RESTRAT2 DDEPTH P1))
64400 (T (RESTRATS DDEPTH P1)))
64500 SRGA P6
64600 (GO SPQ6)
64700 SPQ5 (SETQ PFLG T)
64800 SPQ6 (SETQ Z1
64900 (LIST STRATEGY
65000 SUPPORT
65100 EDITSTRAT
65200 MERGE
65300 ORDER
65400 DEBUG
65500 DEPTH
65600 LENGTH
65700 ANCESTRY
65800 PMODEL
65900 NMODEL
66000 PFLG
66100 EQUAL
66200 PDEPTH
66300 DLIST))
66400 (OUTC CHAN NIL)
66500 (COND (FLG (RETURN (CONS XYZ1 Z1))) (T (RETURN Z1)))))
66600 EXPR)
66700
66800 (DEFPROP SETUP
66900 (LAMBDA(Z)
67000 (PROG (BL Z1 Z2 Z3 Z4 Z5)
67100 SET2 (SETQ Z3 (CAR Z))
67200 (SETQ Z2 0)
67300 (SETQ BL NIL)
67400 (SETQ NO* NO)
67500 (SETQ Z5 NIL)
67600 S1 (SETQ Z4 (MIN1 Z3))
67700 (COND ((NULL Z4) (GO S3)))
67800 (UPIT Z4)
67900 (COND ((MEMBER Z4 Z5) (GO S1)) ((POS Z4) (COND ((MEMBER (CONS ESCAPE Z4) Z5) (GO S4)))))
68000 (SETQ Z2 (ADD1 Z2))
68100 (SETQ Z5 (CONS Z4 Z5))
68200 (GO S1)
68300 S3 (SETQ Z3 NIL)
68400 (SETQ Z4 Z5)
68500 S2 (COND ((NEG (CAR Z4)) (SETQ Z3 Z4) (GO SET3)))
68600 (SETQ Z4 (CDR Z4))
68700 (COND (Z4 (GO S2)))
68800 SET3 (SETQ Z5 (CONS (CONS Z2 (CONS Z3 (CONS 0 (CONS AXNO AXNO)))) Z5))
68900 SET1 (SETQ Z1 (CONS Z5 Z1))
69000 S4 (SETQ Z (CDR Z))
69100 (COND (Z (GO SET2)))
69200 (RETURN Z1)))
69300 EXPR)
69400
69500 (DEFPROP TREE
69600 (LAMBDA(L)
69700 (COND ((ATOM (CDR (ANCESTOR L))) (LIST L))
69800 (T (NCONC (LIST L) (TREE (CAR (ANCESTOR L))) (TREE (CDR (ANCESTOR L)))))))
69900 EXPR)
70000
70100 (DEFPROP TREEDEP
70200 (LAMBDA(X)
70300 (PROG (Z)
70400 (SETQ Z (ANCESTOR X))
70500 (COND ((ATOM (CDR Z)) (RETURN 0)) (T (RETURN (ADD1 (MAX (TREEDEP (CAR Z)) (TREEDEP (CDR Z)))))))))
70600 EXPR)
70700
70800 (DEFPROP TRY1
70900 (LAMBDA(L)
71000 (PROG (FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
71100 (SETQ PRNO 0)
71200 T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
71300 (SETQ Z (CAR (LAST L)))
71400 (SETQ FILENAM (EXPLODE (COND ((ATOM Z) Z) (T (CAR Z)))))
71500 (EVAL (CONS (QUOTE INPUT) L))
71600 (INC T)
71700 P3 B (SETQ Z2 (INCLAUSES))
71800 (INC NIL)
71900 (COND ((NULL Z2) (RETURN NIL)))
72000 (SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
72100 (SETQ Z2 (ATTEMPT Z2 NIL NIL))
72200 A (COND ((NULL Z2) (RETURN (QUOTE *)))
72300 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL)))
72400 ((EQ (CAR Z2) (QUOTE ABORT))
72500 (SETQ Z2 (ATTEMPT (INITIALAX1 (APPEND (CADR Z2) (CDDR Z2))) NIL NIL))))
72600 (GO A)))
72700 FEXPR)
72800
72900 (DEFPROP TRAVERSE
73000 (LAMBDA(L)
73100 (PROG (Z Z1 Z2)
73200 (SETQ Z (ANCESTOR L))
73300 (SETQ Z1 (CAR Z))
73400 (SETQ Z (CDR Z))
73500 (COND ((NOT (ATOM (CDR (ANCESTOR Z)))) (SETQ Z2 (TRAVERSE Z))))
73600 (COND ((NOT (ATOM (CDR (ANCESTOR Z1)))) (SETQ Z2 (NCONC (TRAVERSE Z1) Z2))))
73700 (RETURN (COND ((HERE L) (CONS L Z2)) (T Z2)))))
73800 EXPR)
73900
74000 (DEFPROP UPDATE
74100 (LAMBDA(E)
74200 (PROG (USINGFL USING
74300 CHAN1
74400 ELOC
74500 CHAN
74600 AUTO
74700 DL1
74800 RF
74900 XYZ
75000 XYZ1
75100 CMD
75200 LOCFLG
75300 Z
75400 Z1
75500 Z2
75600 INCT
75700 Z3
75800 UEX
75900 Z1R
76000 Z2R
76100 N1
76200 R
76300 N
76400 NAME
76500 NAMELIST
76600 ZZ)
76700 (SETQ CHAN (OUTC NIL NIL))
76800 (SETQ AXNO (QUOTE INSERT))
76900 (SETQ FNNAM (QUOTE EDI))
77000 (SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
77100 (SETQ N1 (LAST NAMELIST))
77200 (SETQ INCT (INC NIL))
77300 U9 (SETQ ELOC E)
77400 (SETQ N 1)
77500 U3 (UP1A (CAR ELOC) N)
77600 U3A (TERPRI)
77700 U3AA (SETQ CMD (READ))
77800 (COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
77900 U3B (COND ((NOT (ATOM CMD)) (GO UPDATE1)))
78000 U3C (SETQ CMD (EXPLODE CMD))
78100 (COND ((EQ (LENGTH CMD) 1) (GO UER1))
78200 ((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
78300 UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
78400 (GO U3A)
78500 UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
78600 (GO U3A)
78700 UDI1 (SETQ Z1 (UPGETL E NAMELIST))
78800 (COND ((NULL Z1) (GO U3A)))
78900 (CLAUSES Z1)
79000 (GO U3A)
79100 USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
79200 (SETQ Z NAMELIST)
79300 USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
79400 (SETQ Z (CDR Z))
79500 (COND (Z (GO USY2)))
79600 (GO U3A)
79700 UFL2 (SETQ Z (QUOTE U))
79800 (GO UFL4)
79900 UFL3 (SETQ Z (QUOTE D))
80000 (GO UFL4)
80100 UFL1 (SETQ Z (CAR (EXPLODE (READ))))
80200 UFL4 (SETQ Z2 405104)
80300 (COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
80400 UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
80500 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (GO U3A)))
80600 (UPDATESTATE (CDDR Z))
80700 (GO U3A)
80800 UDE1 (SETQ Z2 (UPGETL E NAMELIST))
80900 (COND ((NULL Z2) (GO U3A)))
81000 (EXPUNGE Z2)
81100 (GO U3A)
81200 UIN1 (SETQ NAME (READ))
81300 (SETQ Z2 (UPGETL E NAMELIST))
81400 (COND ((NULL Z2) (GO U3A)))
81500 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
81600 (NCONC Z1 Z2)
81700 (GO U3A)
81800 USU1 (SETQ Z1 (ERRSET (GETTERMS)))
81900 (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
82000 ((NULL (CAR Z1)) (GO U3A)))
82100 (SETQ Z3 NIL)
82200 (SETQ Z1 (CAR Z1))
82300 USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
82400 (SETQ Z1 (CDR Z1))
82500 (COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (GO U12B)))
82600 UUP1 (SETQ Z2 (UPGETNU))
82700 (COND ((NUMBERP Z2) (GO U8)) (T (GO U3A)))
82800 UDO1 (SETQ Z2 (UPGETNU))
82900 (COND ((NUMBERP Z2) (GO U7)) (T (GO U3A)))
83000 UAN1 (SETQ Z2 (UPGETL E NAMELIST))
83100 UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
83200 (SETQ Z2 (CDR Z2))
83300 (GO UAN2)
83400 UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
83500 (INC INCT)
83600 (OUTC CHAN NIL)
83700 (SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
83800 (SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
83900 (RETURN (MINIMIZE (APPEND Z1 Z)))
84000 USA1 (SETQ Z2 (UPGETL E NAMELIST))
84100 (COND (Z2 (NCONC E Z2)))
84200 (GO U3A)
84300 UPA1 (SETQ Z1 (UPGETL E NAMELIST))
84400 (SETQ Z2 (UPGETL E NAMELIST))
84500 (COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
84600 USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
84700 (COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
84800 (COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
84900 (SETQ Z3 Z1)
85000 USI2 (DEMOD (LIST (CAR Z3)) Z2)
85100 (SETQ Z3 (CDR Z3))
85200 (COND (Z3 (GO USI2)))
85300 (PRINT (QUOTE CLAUSES-ARE:))
85400 (CLAUSES Z1)
85500 (GO U3A)
85600 UAS1 (SETQ NAME (QUOTE ASSUMPTIONS))
85700 (GO UUS3)
85800 UCU1 (QUERY)
85900 (GO U3A)
86000 UDS1 (SETQ Z1 (READ))
86100 (COND ((NOT (ATOM Z1)) (GO UDS3)))
86200 UDS2 (COND
86300 ((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
86400 (GO UDS2)))
86500 UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
86600 (GO U3A)
86700 UEO1 (OUTC CHAN1 T)
86800 (GO U3A)
86900 UUS1 (SETQ NAME (QUOTE %USING))
87000 (SETQ USINGFL T)
87100 (SETQ USING NIL)
87200 UUS3 (SETQ LOCFLG T)
87300 UUS2 (SETQ Z2 (UPGETL E NAMELIST))
87400 (SETQ USINGFL NIL)
87500 (COND ((NULL Z2) (GO U3A)))
87600 USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
87700 (COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
87800 (T (RPLACA (CAR N1) NAME)
87900 (RPLACD (CAR N1) Z2)
88000 (RPLACD N1 (CONS (CONS NIL NIL) NIL))
88100 (SETQ N1 (CDR N1))))
88200 (GO U3A)
88300 USE1 (SETQ NAME (READ))
88400 (SETQ LOCFLG NIL)
88500 (GO UUS2)
88600 UCL1 (SETQ Z (READ))
88700 UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
88800 ((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
88900 (GO UCL2))
89000 (T (GO U3A)))
89100 UGO1 (SETQ Z1 (UPGETNU))
89200 (COND ((NOT (NUMBERP Z1)) (GO U3A)))
89300 (COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
89400 (T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
89500 UTR1 (SETQ UEX NIL)
89600 (GO UEX2)
89700 UEX1 (SETQ UEX T)
89800 UEX2 (SETQ NAME (QUOTE LEMMA))
89900 (SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
90000 (COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
90100 (SETQ AUTO T)
90200 (SETQ Z2
90300 (ATTEMPT (INITIALAX (CONS (QUOTE THEOREM) (APPEND XYZ USING)))
90400 (COND (UEX (RESET (DLIST (GETNAME (QUOTE DLIST) NAMELIST)) (STRATEGY (SUPPORT XYZ))))
90500 (T NIL))
90600 NIL))
90700 (SETQ AUTO NIL)
90800 (GO AT1A)
90900 UST1 (STOP)
91000 (GO U3A)
91100 UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
91200 (ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
91300 U8 (COND ((EQ Z2 0) (GO U9)))
91400 U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
91500 (SETQ Z2 (DIFFERENCE Z2 5))
91600 (SETQ ZZ 5)
91700 U84 (SETQ Z N)
91800 (SETQ Z3 (DIFFERENCE N ZZ))
91900 (COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
92000 (SETQ N Z3)
92100 (SETQ Z3 ELOC)
92200 (SETQ ELOC (DOWN N E))
92300 (SETQ ZZ NIL)
92400 (SETQ Z1 ELOC)
92500 U81 (COND ((EQ Z1 Z3) (GO U82)))
92600 (SETQ ZZ (CONS (CAR Z1) ZZ))
92700 (SETQ Z1 (CDR Z1))
92800 (GO U81)
92900 U82 (COND ((NULL ZZ) (GO U83)))
93000 (UP1A (CAR ZZ) (SUB1 Z))
93100 (SETQ ZZ (CDR ZZ))
93200 (SETQ Z (SUB1 Z))
93300 (GO U82)
93400 U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
93500 (SETQ Z2 (PLUS Z2 N))
93600 U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
93700 (SETQ ELOC (CDR ELOC))
93800 (SETQ N (ADD1 N))
93900 (UP1A (CAR ELOC) N)
94000 (COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
94100 UPR1 (TERPRI)
94200 (SETQ Z2 (UPGETL E NAMELIST))
94300 (COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
94400 (COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
94500 (SETQ AXNO (QUOTE THEOREM))
94600 (SETQ Z3 (NEGATE (CAR Z2)))
94700 (SETQ AXNO (QUOTE INSERT))
94800 (SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
94900 (COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
95000 (SETQ NAME (QUOTE LEMMA))
95100 (SETQ LOCFLG T)
95200 (GO USE2)
95300 UME1 (SETQ Z1 (UPGETL E NAMELIST))
95400 (SETQ Z2 (UPGETL E NAMELIST))
95500 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
95600 (BAKSUB Z1 Z2)
95700 (GO U3A)
95800 UHE1 (PRINT MESSAGE)
95900 (GO U3A)
96000 URE1 (SETQ Z1 (UPGETL E NAMELIST))
96100 (SETQ Z2 (UPGETL E NAMELIST))
96200 U%RE1
96300 (SETQ RF T)
96400 URE1A
96500 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
96600 (SETQ Z1R Z1)
96700 (SETQ Z2R Z2)
96800 (SETQ Z3 NIL)
96900 (COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
97000 (COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
97100 UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
97200 ((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
97300 (COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
97400 (COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
97500 (SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
97600 UR3A (SETQ Z2R (CDR Z2R))
97700 (COND (Z2R (GO UR3)))
97800 (SETQ Z1R (CDR Z1R))
97900 (COND (Z1R (SETQ Z2R Z2) (GO UR3)))
98000 UR3B (COND ((NULL Z3)
98100 (COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
98200 (T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
98300 (RF (SETQ NAME (QUOTE RES)))
98400 (T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
98500 (SETQ Z2 Z3)
98600 (SETQ LOCFLG T)
98700 (GO AT2A)
98800 UEV1 (PRINT (QUOTE EVAL-AWAITS))
98900 (SETQ Z2 (ERRSET (EVAL (READ)) T))
99000 (COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
99100 UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
99200 (GO UEV1)
99300 UPDATE1
99400 (SETQ Z (EXPLODE (CAR CMD)))
99500 (COND ((SETQ Z (ASSOC (READLIST (LIST (CAR Z) (CADR Z))) GOLIST1)) (GO (CDR Z))) (T (GO UER1)))
99600 AT1 (COND ((NULL (SETQ Z1 (GETNAME (CADR CMD) NAMELIST))) (GO U3A)))
99700 (SETQ NAME (CADR CMD))
99800 (SETQ XYZ Z1)
99900 (RPLACA (CDR CMD) (QUOTE XYZ))
00100 (RPLACA CMD (QUOTE ATTEMPTUNTIL))
00200 (SETQ Z2 (EVAL CMD))
00300 AT1A (UPDATESTATE STRAT)
00400 (COND
00500 ((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
00600 (PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
00700 (PRINC NAME)
00800 (GO U3A))
00900 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
01000 (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
01100 (SETQ AUTO NIL)
01200 (GO AT1A))
01300 ((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
01400 (SETQ Z2 (CADR Z2))
01500 AT2A (SETQ N 1)
01600 AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
01700 (SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
01800 (PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
01900 (PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
02000 (PRIN1 NAME)
02100 (CLAUSES Z2)
02200 (GO USE2)
02300 S1 (COND ((NULL (SETQ XYZ (GETNAME (CADDDR CMD) NAMELIST))) (GO U3A)))
02400 (RPLACA (CDDDR CMD) (QUOTE XYZ))
02500 (RPLACA CMD (QUOTE SAVE))
02600 (EVAL CMD)
02700 (GO U3A)))
02800 EXPR)
02900
03000 (DEFPROP UPGETL
03100 (LAMBDA(E N)
03200 (PROG (C N1 Z Z1 Z2 Z3 ZZ N2)
03300 (SCANSET)
03400 (START)
03500 (SETQ C (ERRSET (<CLAUSES>) T))
03600 (SCANRESET)
03700 (COND ((OR (NULL C) (NULL (CAR C))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
03800 (SETQ C (TOP))
03900 (COND ((EQ C (QUOTE EMPTY)) (RETURN NIL)))
04000 AS1 (SETQ Z (CAR C))
04100 (COND ((ATOM Z)
04200 (COND ((NUMBERP Z) (SETQ N2 (QUOTE CLAUSES))
04300 (COND ((SETQ Z1 (DOWN Z E)) (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1)))))
04400 (T (RETURN NIL))))
04500 ((SETQ Z1 (GETNAME Z N)) (SETQ N2 Z) (SETQ ZZ (APPENDIT ZZ Z1)))
04600 (T (RETURN NIL))))
04700 ((EQ (CAR Z) (QUOTE STAT)) (GO AS10))
04800 ((EQ (CAR Z) (QUOTE FIND)) (GO AS20))
04900 ((EQ (CAR Z) (QUOTE DSK)) (GO AS30))
05000 ((SETQ Z1 (GETNAME (CAR Z) N)) (SETQ N2 (CAR Z)) (GO AS2))
05100 (T (RETURN NIL)))
05200 AS6 (SETQ C (CDR C))
05300 (COND (C (GO AS1)) (T (RETURN ZZ)))
05400 AS2 (SETQ Z2 (CADR Z))
05500 (SETQ N1 (CAR Z))
05600 (SETQ Z (CDR Z))
05700 (SETQ Z3 Z1)
05800 AS2A (COND ((NOT (NUMBERP Z2)) (PRINT (QUOTE NON-NUMERIC-ARG-FOR:)) (PRINC N1) (RETURN NIL)))
05900 AS3 (SETQ Z2 (SUB1 Z2))
06000 (COND ((ZEROP Z2) (GO AS4)))
06100 (SETQ Z1 (CDR Z1))
06200 (COND (Z1 (GO AS3)) (T (PRINT (QUOTE EXCEEDED-SIZE-OF:)) (PRINC N1) (RETURN NIL)))
06300 AS4 (COND
06400 ((NOT (HERE (CAR Z1))) (PRINT N1)
06500 (PRINC (QUOTE / ))
06600 (PRINC (CAR Z))
06700 (PRINC (QUOTE / ))
06800 (PRINC (QUOTE HAS-BEEN-DELETED))
06900 (RETURN NIL)))
07000 (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1))))
07100 (SETQ Z (CDR Z))
07200 (COND (Z (SETQ Z1 Z3) (SETQ Z2 (CAR Z)) (GO AS2A)))
07300 (GO AS6)
07400 AS10 (SETQ N2 (QUOTE INSERT))
07500 (SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF (FIXQFF (CDR Z)))))))
07600 (GO AS6)
07700 AS20 (SETQ N2 (QUOTE MATCHES))
07800 (SETQ Z (MAPIT (CADR Z) (LIST (QUOTE FUNCTION) (LIST (QUOTE LAMBDA) (QUOTE (C)) (CADDR Z))) N))
07900 (COND ((NULL Z) (GO AS6)) (T (GO AS31)))
08000 AS30 (SETQ N2 (QUOTE INPUT))
08100 (SETQ ZIN (CDR Z))
08200 (COND
08300 ((NULL (ERRSET (EVAL (LIST (QUOTE INPUT) (QUOTE DSK:) ZIN)))) (PRINT (QUOTE CONTINUING)) (GO AS6)))
08400 (INC T)
08500 (SETQ Z (INCLAUSES))
08600 (INC NIL)
08700 (COND ((NULL Z) (RETURN NIL)))
08800 AS31 (SETQ ZZ (APPENDIT ZZ Z))
08900 (GO AS6)))
09000 EXPR)